DROPS

Document

DOI: 10.4230/LIPIcs.STACS.2024.12

Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form

Authors: Christoph Berkholz, Dietrich Kuske, and Christian Schwarz

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract

Is it possible to write significantly smaller formulae, when using more Boolean operators in addition to the De Morgan basis (and, or, not)? For propositional logic a negative answer was given by Pratt: every formula with additional operators can be translated to the De Morgan basis with only polynomial increase in size. Surprisingly, for modal logic the picture is different: we show that adding bi-implication allows to write exponentially smaller formulae. Moreover, we provide a complete classification of finite sets of Boolean operators showing they are either of no help (allow polynomial translations to the De Morgan basis) or can express properties as succinct as modal logic with additional bi-implication. More precisely, these results are shown for the modal logic T (and therefore for K). We complement this result showing that the modal logic S5 behaves as propositional logic: no additional Boolean operators make it possible to write significantly smaller formulae.

Cite as

Christoph Berkholz, Dietrich Kuske, and Christian Schwarz. Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.STACS.2024.12,
  author =	{Berkholz, Christoph and Kuske, Dietrich and Schwarz, Christian},
  title =	{{Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.12},
  URN =		{urn:nbn:de:0030-drops-197228},
  doi =		{10.4230/LIPIcs.STACS.2024.12},
  annote =	{Keywords: succinctness, modal logic}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2020.61

Complexity of Counting First-Order Logic for the Subword Order

Authors: Dietrich Kuske and Christian Schwarz

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract

This paper considers the structure consisting of the set of all words over a given alphabet together with the subword relation, regular predicates, and constants for every word. We are interested in the counting extension of first-order logic by threshold counting quantifiers. The main result shows that the two-variable fragment of this logic can be decided in two-fold exponential space provided the regular predicates are restricted to piecewise testable ones. This result improves prior insights by Karandikar and Schnoebelen by extending the logic and saving one exponent. Its proof consists of two main parts: First, we provide a quantifier elimination procedure that results in a formula with constants of bounded length (this generalizes the procedure by Karandikar and Schnoebelen for first-order logic). From this, it follows that quantification in formulas can be restricted to words of bounded length, i.e., the second part of the proof is an adaptation of the method by Ferrante and Rackoff to counting logic and deviates significantly from the path of reasoning by Karandikar and Schnoebelen.

Cite as

Dietrich Kuske and Christian Schwarz. Complexity of Counting First-Order Logic for the Subword Order. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 61:1-61:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kuske_et_al:LIPIcs.MFCS.2020.61,
  author =	{Kuske, Dietrich and Schwarz, Christian},
  title =	{{Complexity of Counting First-Order Logic for the Subword Order}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{61:1--61:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.61},
  URN =		{urn:nbn:de:0030-drops-127297},
  doi =		{10.4230/LIPIcs.MFCS.2020.61},
  annote =	{Keywords: Counting logic, piecewise testable languages}
}

Search Results

Documents authored by Schwarz, Christian

Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form

Abstract

Cite as

Complexity of Counting First-Order Logic for the Subword Order

Abstract

Cite as

Thanks for your feedback!

Could not send message